basic
\\[0ex]fun\_thru\_1op($A$;$B$;${\it opa}$;${\it opb}$;$f$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\forall$$a$:$A$. $f$(${\it opa}$($a$)) = ${\it opb}$($f$($a$))